$\forall$$i$:Id, $A$:MsgA, $P$:(Id$\rightarrow\mathbb{B}$), $L$:(\{${\it loc}$:Id$\mid$ $P$(${\it loc}$) \}$\rightarrow$(MsgA List)).
\\[0ex]($\forall$${\it loc}$:Id. ($\forall$$A$,$B$$\in$if $P$(${\it loc}$)$\rightarrow$ $L$(${\it loc}$) else nil fi.$A$ $\Vert\!+$ $B$))
\\[0ex]$\Rightarrow$ $P$($i$)
\\[0ex]$\Rightarrow$ ($\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$($i$)$\parallel$}}$. $A$ $\subseteq$ $L$($i$)[$n$] $\Rightarrow$ @$i$: $A$ $\subseteq$ $\lambda$${\it loc}$.$\oplus$(if $P$(${\it loc}$)$\rightarrow$ $L$(${\it loc}$) else nil fi))